(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const _5-0 (_ BitVec 5))
(assert (xor v4 v13 v15 v0 v4 v16 v15 v16 v13))
(declare-const v17 Bool)
(assert (=> v15 v4))
(assert v13)
(assert (or (xor v4 v13 v15 v0 v4 v16 v15 v16 v13) v14 v8 v1 v2 v7))
(declare-const _10-0 (_ BitVec 10))
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (xor (distinct _5-0 (bvxor _5-0 _5-0 _5-0 _5-0) (bvxor _5-0 _5-0 _5-0 _5-0)) v11 v12 v13 (and v6 v13 v1 v14 (=> v15 v4) v12 v14 v4 (or (xor v4 v13 v15 v0 v4 v16 v15 v16 v13) v14 v8 v1 v2 v7))))
(assert v19)
(assert (xor v5 v5 (bvult (bvxor _5-0 _5-0 _5-0 _5-0) (bvxor _5-0 _5-0 _5-0 _5-0)) (=> v15 v4) v7 v17 v2))
(declare-const v20 Bool)
(assert (bvult (bvxor _5-0 _5-0 _5-0 _5-0) _5-0))
(declare-const v21 Bool)
(assert v16)
(assert (exists ((q0 Bool) (q1 (_ BitVec 14)) (q2 (_ BitVec 21))) (=> (bvule (concat _10-0 #b01110110111) q2) (distinct ((_ sign_extend 5) (_ bv355 9)) ((_ sign_extend 5) (_ bv355 9)) ((_ sign_extend 5) (_ bv355 9)) q1))))
(declare-const v22 Bool)
(assert (not v1))
(declare-const v23 Bool)
(assert v18)
(check-sat)
